\documentclass[a4paper,10pt]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[english]{babel}
%\usepackage{bookman}
%\usepackage{pxfonts}

%\usepackage[T1]{fontenc}
\usepackage{subfig}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{a4wide}
\usepackage{hyperref}
\pagestyle{headings}
\pagestyle{plain}
\usepackage{url}

\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}

\newcommand{\mint}[1]{\;\mathrm{#1}}
\newcommand{\then}{\Rightarrow}

\newcommand{\w}{\mathbf{w}}
\renewcommand{\c}{\mathbf{c}}
\newcommand{\1}{\mathbf{1}}


%\frenchspacing

\title{Automatic reasoning, assignment 1 \\ Truck loading}
\author{Niklas Weber \\ 0841420, \\ Matúš Tejiščák \\ 4176200}
\date{\today}

\begin{document}

\maketitle

\section{Representation}

Having $G$ goods and $N$ trucks, we can represent any solution as an $N \times G$ matrix $L$,
symbolizing that the truck $n$ carries $L_{ng}$ pallets of the goods $g$.
\begin{equation}
	L = \left(
	\begin{matrix}
		L_{11} & L_{12} & L_{13} & \cdots & L_{1G} \\
		L_{21} & L_{22} & L_{23} & \cdots & L_{2G} \\
		L_{31} & L_{32} & L_{33} & \cdots & L_{3G} \\
		       & \vdots &        & \ddots & \vdots \\
		L_{N1} & L_{N2} & L_{N3} & \cdots & L_{NG}
	\end{matrix} \right)
\end{equation}

We represent the weight of each goods as a column vector $\w$ of type $G \times 1$ and
the required count of pallets for each goods as a vector $\c$, also of type $G \times 1$.
\begin{equation}
	\w = \left(
	\begin{matrix}
		w_1 \\ w_2 \\ w_3 \\ \vdots \\ w_G
	\end{matrix} \right); \quad
	\c = \left(
	\begin{matrix}
		c_1 \\ c_2 \\ c_3 \\ \vdots \\ c_G
	\end{matrix} \right)
\end{equation}

Let us also use the name $w_{\max}$ for the maximum load of each truck and $c_{\max}$
for the maximum count of pallets for each truck. Then we have the following constraints:
\begin{align}
	L_{ng} &\geq 0
		& \text{(consistency of load)} \\
	L^T \cdot [1]_{N \times 1} &= \c
		& \text{(required count of pallets per each goods)} \\
	L \cdot [1]_{G \times 1} &\leq [c_{\max}]_{N \times 1}
		& \text{(space constraints for each truck)} \\
	L \cdot \w &\leq [w_{\max}]_{N \times 1}
		& \text{(weight constraints for each truck)}
\end{align}

This is all it takes to encode this problem. The length of the encoding is obviously
$O(NG)$, since we have three vector (in)equations, each dealing with a single matrix-time-vector
expression that is compared to another vector (the first inequality is obviously $O(NG)$).

\section{Implementation}

We solved this task using \textsf{Yices}, encoding the problem in a \textsf{Haskell} EDSL
designed for this purpose. In the \textsf{Haskell} program\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task1.hs}
}, we defined functions with rather
intuitive names instead of using direct matrix operations (although the functions essentially
don't encode anything more than matrix operations).

The \textsf{Haskell} EDSL gives us the convenience of expressing the formulas in a compact way
(using recursion, quantifiers, abstraction etc.), while it automatically expands the formulas
into first-order terms behind the scenes.

We also used a custom data type for the goods. Thus, we do not represent the goods using numbers
but using a specialized data type for readability.

Finding the maximum count of beer pallets was done by varying the beer-related component
of the vector $\c$ and seeing whether the resulting formula is still satisfiable.

\section{Solution}

We discovered that the maximum number of beer pallets that can be loaded is 19. A possible
load distribution in that case is given below.

\begin{table}[htp]
	\centering{
	\begin{tabular}{cccccc}
		truck & cheese & beer & wine & drinks & chips \\
		1& 2&2&3&1&0 \\
		2& 1&6&0&0&0 \\
		3& 0&3&3&1&1 \\
		4& 0&1&1&4&2 \\
		5& 0&3&0&3&1 \\
		6& 1&4&1&1&1 \\
		\hline
		&4&19&8&10&5\\
	\end{tabular}
	}
	\caption{An optimal solution: we can load 19 pallets of beer.}
\end{table}


\end{document}




























